\begin{tabbing}
$\forall$\=${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}, $p$,\+
\\[0ex]${\it p'}$:(\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$Prop).
\-\\[0ex]($\forall$$e$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}. $p$($e$) $\Leftrightarrow$ ${\it p'}$($e$))
\\[0ex]$\Rightarrow$ ($e_{2}$ = first $e$ $\geq$ $e_{1}$.$p$($e$) $\Leftrightarrow$ $e_{2}$ = first $e$ $\geq$ $e_{1}$.${\it p'}$($e$))
\end{tabbing}